a:, p:FinProbSpace, F:(Outcome). (x:Outcome. F(x) = a)  (weighted-sum(p;F) = a) 

latex

Definitions	, t  T, ||as||, a < b, P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , {i..j}, Void, x:AB(x), x:A. B(x), (x  l), #$n, r  s, x. t(x), xL. P(x), l[i], a  j < b. E(j), s = t, x:A  B(x), type List, Type, f(a), , <a, b>, weighted-sum(p;F), Outcome, FinProbSpace, True, P  Q, T, r * s, P  Q, x.A(x), , x:A.B(x), Top, S  T, s ~ t, {T}, SQType(T), x,y:A//B(x;y)
Lemmas	qmul one qrng, prod sum l q, length wf nat, top wf, nat wf, qmul wf, squash wf, true wf, qsum wf, length wf1, select wf, int seg wf, l all wf2, qle wf, int inc rationals, l member wf, rationals wf